COMMENT ⊗   VALID 00003 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	.require "memo.pub[let,jmc]" source
C00014 00003	.skip 1
C00015 ENDMK
C⊗;
.require "memo.pub[let,jmc]" source;
.AT "qt" ⊂"%At%*"⊃
.AT "qw" ⊂"%Aw%*"⊃
.AT "qi" ⊂"%5 -1%*"⊃
.AT "qm" ⊂"%Am%*"⊃
.every heading (,draft,{page})
.cb EXOTIC CONTINUOUS FUNCTIONALS


.bb "1. Some examples of exotic continuous functionals."

	The fixed point theory of recursive functions is based on
continuous functionals such as qt defined by

!!a1:	%2qt[f](x) = qif p x qthen g x qelse m(x,f h x)%1.

	The theory tells us that each continuous monotonic functional
has a fixed point, and we study the fixed points of those functionals
involved in recursive definitions.  In the case of recursive definitions
%2qt[f](x)%1 is a form in which ⊗f appears as a function symbol.
However, these are not all the
continuous functions there are, and it may be interesting to study
some other examples.  Consider functionals of the form

!!a2:	%2qt[f](x) = qif p x qthen g x qelse m fqi h x%1;

that's right, we mean the inverse of the function %2f%1.  In order
to make the functional well defined and continuous, we make the
following stipulations:  First, the variable ⊗x ranges over non-negative
integers and ⊗f is a partial function from integers to integers.
Second, we define %2fqi%1 by

!!a3:	%2fqi(y) = qm x.(f(x) = y)%1,

where

!!a6:	%2qm x.p(x) ← least(0,p)%1,

and %2least(y,p)%1 is recursively defined by

!!a7:	%2least(y,p) ← qif p(y) qthen y qelse least(y+1,p)%1.

Note that the recursive definition insures that %2fqi%1 is continuous
in ⊗f, and that qmx.%2p(x)%1 is undefined if there is a value of
⊗x for which ⊗p(x) is undefined lower than a value for which ⊗p(x) 
is true.  Without this property, %2least(x,p)%1 wouldn't be monotonic
in %2p%1, and there mightn't be a least fixed point.

	Consider specializing ({eq a2}) to

!!a4:	%2qt1[f](x) = qif x = 0 qthen 0 qelse 2 + fqi(x - 1)%1.

The fixed point ⊗f1 of qt1 may be computed by iterating qt1 on %AW%1,
getting

!!a5:	%2f1 x = qif x = 0 qthen 0 qelse qif x = 1 qthen 2 qelse qif
x = 3 qthen 3 qelse qw%1,

which seems exotic if not pathological.

	Wolf Polak points out that while qt1 is exotic, its fixed point
is an ordinary recursive function, since the recursive computation
of %2fqi%1 can be spelled out.  Thus

!!a8:	%2f1 x ← qif x = 0 qthen 0 qelse 2 + f2(0,x-1)%1,

where

!!a9:	%2f2(y,x) ← qif f1(x) = y qthen x qelse f2(y+1,x)%1.

	Here is another weird functional:

!!a10:	%2qt2[f](x) = qif p x qthen g x qelse qif
f h1 x = qw ∧ f h2 x = qw qthen qw qelse f h3 x%1,

where ⊗p, ⊗g, ⊗h1, ⊗h2 and ⊗h3 are all assumed total.  (Equality here is
taken in the strong sense in which its value is always %3true%1 or %3false%1
and is never undefined).
Computing %2qt2[f](x)%1
involves a parallel computation of %2f h1 x%1 and %2f h2 x%1;
if either succeeds, the other can be stopped.  It is easily seen that the
functional is continuous and hence has a fixed point - call it ⊗f2. 
If we can use Lisp functions, we can write an ordinary recursive
definition of ⊗f2, namely

!!a11:	%2f2 x ← qif p x qthen g x qelse (λy. f2 h3 x)(f2'(list(x),qNIL))%1,

with

!!a12:	%2f2'(u,v) ← qif qn u qthen (qn v ∨ f2(v,qnil))
qelse p h1 qa u ∨ p h2 qa u ∨ f2'(qd u, h1 qa u . (h2 qa u . v))%1.

[Carolyn Talcott points out that the above redefinition is not
correct and has an alternate breadth first search, but hadn't proved
hers correct to her satisfaction at last discussion].

If we are not allowed to use Lisp functions, then ⊗f2 may be one of
Hewitt's and Paterson's (197x) examples of functions that can be written
with parallel programs but not with recursive programs.


.bb "2. When is a functional definable by a term?"

	In view of the above examples, we can try to characterize
those continuous functional for which %2qt[f](x)%1 can be written
as a term in ⊗f and ⊗x in which ⊗f appears as a function symbol and
⊗x as an individual variable.  Let's call them %2term functionals%1.

	If qt is a continuous functional, then the value of
%2qt[f](x)%1 depends on the value of ⊗f(y) for only a finite
number of %2y%1's.  Namely, there exist %2y%41%2,_..._,y%4k%1
such that ⊗f(y) can be changed for any ⊗y different from the %2y%4i%1's
without changing the value of %2qt[f](x)%1.  In general ⊗k depends
on the particular ⊗f and ⊗x, but when qt is a term functional, ⊗k is
bounded by the number of occurrences of ⊗f in the term %2qt[f](x)%1.
In our first exotic example, the number of ⊗f(y) on which %2qt[f](x)%1
depends is unbounded, because, depending on ⊗f, any finite number of
of %2f(x)%1's may have to be examined to compute %2fqi(y)%1.
Tentatively, we shall call a functional where such a bound exists
%2uniformly continuous%1, although we have not yet been able to
establish any properties in common with the corresponding property
in analysis.  Thus all %2term functionals%1 are %2uniformly continuous%1.

	The second exotic functional is uniformly continuous but still
isn't a term functional.  Indeed every term functional has the another
property that we may call %2sequentiality%1:

	Suppose that in evaluating %2qt[f](x)%1, we have already evaluated
%2f(x1),f(x2),_...,f(xk)%1.  There are two possibilities;  Either the
value of %2qt[f](x)%1 is already determined by these values or ⊗f(y) must
be computed for additional %2y%1's.  We call qt %2sequential%1 if
in the latter case there is always at least one ⊗y such that %2qt[f](x)%1_=_qw%1
unless %2f(y)_≠_qw%1.  The function qt2 of the previous section is not
sequential.  If qt is sequential we can always write

!!b6:	%2qt[f](x) = qif p1 x qthen g1 x qelse α{f h1 xα}[λx1.qif p2(x,x1)
qthen g2(x,x1) qelse α{f h2(x,x1)α}[λx2.qif p3(x,x1,x2) qthen g3(x,x1,x2)
qelse α{f h3(x,x1,x2α}[λx3.qif ... etc. ]]]%1.

[We use the notation %2α{argα}fn%1 for %2fn(arg)%1 when it is more convenient
to write the argument before the function].

	We can avoid the lengthening formulas of ({eq b6}) by writing

!!b6a:	%2qt[f](x0) = qif p1 x0 qthen g1 x0 qelse α{m1(x0,f h1 x0)α}[λx1.qif p2 x1
qthen g2 x1 qelse α{m2(x1,f h2 x1)α}[λx2.qif p3 x2 qthen %1etc.

	Given that qt is sequential, there are two possibilities.  If
qt is also %2uniformly continuous%1 the sequence of terms given in ({eq b6})
will be finite - otherwise not.  If the %2p%1's, %2g%1's and %2h%1's
are all computable in some collection %2C%1 of base functions, then we will
call qt computable if it is sequential and bounded.  In that case its
least fixed point will also be a computable function in %2C%1.

	While sequentiality
requires that some %2f(x)%1 be required for the definedness of %2qt[f](x)%1,
it doesn't require that %2h(x)%1 be unique.  Thus if

!!b7:	%2qt[f](x) = f(m x) + f(n x)%1,

we can take either %2h1_x_=_m_x%1 or %2h1_x_=_n_x%1.


.bb "3. Additional remarks."

	1. Here are some more continuous %2qt[f](x)%1:

a. %2f(x) ≠ qw%1 for at least one ⊗x. 

b. %2f(x)+x ε A%1 for at least 20 odd values of ⊗x. 

c. %2R1(x,f h1 x) ∧ R2(x,f f h2 x)%1 for at least 20 ⊗x. 

d. The functional

	%2qt[f](x) = qif p1 x qthen g x qelse qif ∃z.(f h1 z ≠ qw) qthen
f h2 z qelse qw%1

is continuous.  It can't be computed for general ⊗f except by
parallel evaluator, but its fixed point can apparently be sequentially
computed provided the domain of ⊗x can be effectively enumerated.

	2.  Note that ⊗a thru ⊗c above are predicates, and the
essential part of ⊗d is also a predicate.
Predicates play a special role, because
it is easier to define exotic continuous predicates than other functions.
The space whose elements
are just T and qw seems to play a special role.
.skip 1
.begin verbatim
John McCarthy
Artificial Intelligence Laboratory
Computer Science Department
Stanford University
Stanford, California 94305

ARPANET: MCCARTHY@SU-AI
.end

.turn on "{"
%7This draft of
EXOTIC[W77,JMC]
PUBbed at {time} on {date}.%1